;;;COMMENT INST(E,M,P) IS AN A-LIST THAT WILL YIELD E WHEN
;;;SUBSTITUTED IN M.  P IS AN A- LIST OF PREVIOUSLY COMMITED SUBSTITUTIONS,
;;;ORDINARILY NIL.  INST REQUIRES A PREDICATE ISVAR(M) TO IDENTIFY 
;;;VARIABLES.;

(DEFUN INST (E M P) (COND ((EQ P (QUOTE NO)) P) ((ATOM M) (COND ((ISVAR M)
((LAMBDA (W) (COND ((NULL W) (CONS (CONS M E) P))
((EQUAL (CDR W) E) P) (T (QUOTE NO)))) (ASSOC M P)))
((EQ M E) P) (T (QUOTE NO)))) ((ATOM E) (QUOTE NO))
(T (INST (CDR E) (CDR M) (INST (CAR E) (CAR M) P)))))

(DEFUN ISVAR (M) (MEMBER M (QUOTE (U V W X Y Z))))

;;;COMMENT THIS  SUBLIS  CREATES NO UNNECESSARY LIST STRUCTURE.;

(DEFUN SUBLIS (E P) (COND ((ATOM E) 
((LAMBDA (W) (COND ((NULL W) E) (T (CDR W))))
(ASSOC E P)))
(T ((LAMBDA (X Y) (COND ((AND (EQ X (CAR E))
(EQ Y (CDR E))) E) (T (CONS X Y)))) (SUBLIS (CAR E) P)
 (SUBLIS (CDR E) P)))))